Inference at * 2 0 1 3 1 
Iof proof for Lemma multiply nat wf:



1. i : 
2. j : 
3. 0 < j
4. ((j - 1)  0 )  (0  (i * (j - 1)))
5. j  0 
  0  (i * j) 

latex

 by ((Thin (-1)) 
CollapseTHEN (D (-1))) 

latex

C1: .....antecedent..... NILNIL

C1: 3. 0 < j
C1:   (j - 1)  0 
C2: 

C2: 4. 0  (i * (j - 1))
C2:   0  (i * j)
C.

Definitions

n * m, A  B, n - m, i  j , #$n, a < b, , , x:AB(x), P  Q